
#include <algorithm>
#include <atomic>
#include <bitset>
#include <cassert>
#include <chrono>
#include <condition_variable>
#include <cstdlib>
#include <cstring>
#include <fstream>
#include <iomanip>
#include <iostream>
#include <mutex>
#include <optional>
#include <thread>
#include <vector>

#define len(clause) (clause.ref.count())

#define caRESET "\e[0m"
#define caBOLD "\e[1m"
#define fgBLACK "\e[30m"
#define fgRED "\e[31m"
#define fgGREEN "\e[32m"
#define fgBLUE "\e[34m"
#define fgLIGHTRED "\e[91m"
#define bgGRAY "\e[47m"
#define bgDARKGRAY "\e[100m"

typedef std::chrono::high_resolution_clock Clock;

// ==================================================================

const int VAR_NUM = 256;

typedef std::bitset<VAR_NUM> BitSeq;

typedef int32_t Lit;
typedef Lit VarSeq[VAR_NUM];
typedef double VarScr[VAR_NUM];

class Clause {
public:
  BitSeq ref, pol;

  Clause *clone() const {
    Clause *newClause = new Clause();
    newClause->ref = this->ref;
    newClause->pol = this->pol;
    return newClause;
  }

  void rst() {
    ref.reset();
    pol.reset();
  }

  void set(Lit l) {
    assert(l != 0);
    ref[abs(l)] = 1;
    pol[abs(l)] = l > 0;
  }

  void clr(Lit l) {
    ref[abs(l)] = 0;
    pol[abs(l)] = 0;
  }

  void print(int varRange) {
    for (int i = 1; i < varRange; i++)
      if (!ref[i])
        std::cout << bgDARKGRAY " " caRESET;
      else if (pol[i])
        std::cout << bgDARKGRAY caBOLD fgBLACK << "+" caRESET;
      else
        std::cout << bgDARKGRAY caBOLD fgBLACK << "-" caRESET;
    std::cout << "\n";
  }
};

typedef std::vector<Clause *> LitMem;

// ==================================================================

class CantorNode {
  int head, tail;
  CantorNode *pos, *neg;

  CantorNode(int head, int tail)
      : head(head), tail(tail), pos(nullptr), neg(nullptr) {}
};

// ==================================================================
// Helper functions for parsing DIMACS CNF.

char *readWS(char *p) {
  while (1)
    switch (*p) {
    default:
      return p;
    case 9 ... 13:
    case 32:
      ++p;
    }
}

char *readNL(char *p) {
  while (*p != '\n')
    if (*p++ == '\0')
      exit(1);
  return ++p;
}

char *readNum(char *p, int *i) {
  int sgn = 1;
  *i = 0;
  p = readWS(p);
  while (1)
    switch (*p) {
    case 0:
      return p;
    case '-':
      sgn = -1;
      ++p;
      break;
    case '0' ... '9':
      *i = *i * 10 + (*p - '0');
      ++p;
      break;
    default:
      goto done;
    }

done:
  *i *= sgn;
  return p;
}

void parse(char *filename, LitMem &litMem, int &varNum, int &claNum) {

  std::ifstream fin(filename);
  fin.seekg(0, fin.end);
  size_t fileSize = fin.tellg();
  fin.seekg(0, fin.beg);
  char *data = new char[fileSize + 1], *p = data;
  fin.read(data, fileSize);
  fin.close();

  data[fileSize] = '\0';
  Clause *buf = new Clause();
  while (1) {
    p = readWS(p);
    switch (*p) {
    case '%': // special handling for SATLIB benchmarks
    case '\0':
      goto doneParse;
    case 'c':
      p = readNL(p);
      break;
    case 'p':
      if (!memcmp(p, "p cnf", 5)) {
        p += 5, p = readNum(p, &varNum), p = readNum(p, &claNum);
      }
      break;
    default:
      Lit lit;
      p = readNum(p, &lit);
      if (*p == '\0' && lit != 0)
        printf("c PARSE ERROR! Unexpected EOF\n"), exit(1);
      if (lit == 0) {
        litMem.push_back(buf);
        buf = new Clause();
      } else
        buf->set(lit);
    }
  }
doneParse:
  return;
}

// =======================================================================================

std::mutex mut;
std::condition_variable cond;

// All threads finding a solution writes this.

const int max_threads = 128;

void paraRadixSortInner(LitMem &litMem, int varNum, int depth, int head,
                        int tail) {
  if (depth >= varNum || tail - head <= 1)
    return;

  LitMem bins[3];
  bins[0].reserve(tail - head);
  bins[1].reserve(tail - head);
  bins[2].reserve(tail - head);

  for (int i = head; i < tail; i++) {
    int ref = litMem[i]->ref[depth];
    int pol = litMem[i]->pol[depth];
    int dex = !ref + pol * 2;
    bins[dex].push_back(litMem[i]);
  }

  int neck = head + (int)bins[0].size();
  int butt = neck + (int)bins[1].size();
  assert(tail == butt + (int)bins[2].size());

  std::copy(bins[0].begin(), bins[0].end(), litMem.begin() + head);
  std::copy(bins[1].begin(), bins[1].end(), litMem.begin() + neck);
  std::copy(bins[2].begin(), bins[2].end(), litMem.begin() + butt);

  std::thread tp(paraRadixSortInner, std::ref(litMem), varNum, depth + 1, head,
                 neck);
  std::thread ta(paraRadixSortInner, std::ref(litMem), varNum, depth + 1, neck,
                 butt);
  std::thread tn(paraRadixSortInner, std::ref(litMem), varNum, depth + 1, butt,
                 tail);
  tp.join();
  ta.join();
  tn.join();
}

void paraRadixSort(LitMem &litMem, int varNum) {
  std::thread t(paraRadixSortInner, std::ref(litMem), varNum, 1, 0,
                (int)litMem.size());
  t.join();
}

std::atomic<uint> thnum(1);
std::atomic<bool> satis(false);

typedef std::optional<Clause> ClauOp;

typedef struct ProLit {
  Lit lit;
  int lev;
  ClauOp ant;
} ProLit;

typedef std::vector<ProLit> ProMem;

int val(std::shared_ptr<ProMem> proMem, Clause *cRef, Lit &res) {

  Clause c = *cRef; // deref
  Clause v;

  for (auto &p : *proMem)
    v.set(p.lit);

  if ((c.ref & v.ref & ~(c.pol ^ v.pol)).any())
    return 1;

  auto uniMask = c.ref & ~v.ref;

  for (int i = 0; i < VAR_NUM; i++)
    if (uniMask[i])
      res = i * (c.pol[i] ? 1 : -1);

  return -uniMask.count();
}

void assign(std::shared_ptr<ProMem> proMem, int lit, int lev, ClauOp c) {
  ProLit newPro = {lit, lev, c};
  proMem->emplace_back(newPro);
}

ClauOp prop(LitMem &litMem, std::shared_ptr<ProMem> proMem, int &proTop,
            int varNum) {
  Lit res;

  while (proTop < (int)proMem->size()) {
    for (auto &c : litMem) {
      switch (val(proMem, c, res)) {
      case 1:
        break;
      case 0:
        return *c;
      case -1:
        assign(proMem, res, proMem->at(proTop).lev, *c);
      default:; // the case with more than two lits unassigned are not handled.
      }
    }

    proTop++;
  }

  if ((int)proMem->size() == varNum) {
    std::lock_guard<std::mutex> lock(mut);
    satis.store(true);
    cond.notify_all();
  }
  return std::nullopt;
}

int conf(Clause &con, ProMem &proMem, int &proTop, Clause &learnt) {

  learnt.rst();
  if (proMem[proTop].lev == 0)
    return 20;

  int bakPtr = (int)proMem.size() - 1;

  learnt.ref = con.ref;
  learnt.pol = con.pol;

  BitSeq equDecLen;
  for (auto &p : proMem)
    equDecLen[abs(p.lit)] = p.lev == proMem[proTop].lev;

  while (1) {

    if (proMem[bakPtr].ant == std::nullopt)
      assert((learnt.ref & equDecLen).count() == 1);

    if ((learnt.ref & equDecLen).count() == 1)
      break; // condition of finding 1st UIP

    auto reazon = proMem[bakPtr].ant.value(); // next clause on the reason stack

    auto resMask = learnt.ref & reazon.ref &
                   (learnt.pol ^ reazon.pol); // condition of resolution

    if (resMask.any()) {
      learnt.ref = (learnt.ref | reazon.ref) & ~resMask;
      learnt.pol = (learnt.pol | reazon.pol) & ~resMask;
    }

    bakPtr--;
    assert(bakPtr >= 0);
  }

  int resLit = 0;
  auto resLitPos = learnt.ref & equDecLen;
  while (!resLitPos[abs(proMem[bakPtr].lit)] && bakPtr > -1)
    bakPtr--;
  resLit = -proMem[bakPtr].lit;

  if (len(learnt) == 1) {

    proTop = 0;
    proMem.resize(0);
    assign(proMem, resLit, 0, std::nullopt);
  } else {

    auto bakDesPos = learnt.ref & ~equDecLen;

    while (!bakDesPos[abs(proMem[bakPtr].lit)] && bakPtr > -1)
      bakPtr--;
    while (proMem[bakPtr].lev == proMem[bakPtr + 1].lev)
      bakPtr++;
    bakPtr++;

    int nexLev = proMem[bakPtr].lev - 1;
    proTop = bakPtr;
    proMem.resize(bakPtr);
    assign(proMem, resLit, nexLev, learnt);
  }
  return 0;
}

void karnaugh(int varNum, LitMem &litMem, std::shared_ptr<ProMem> proMem,
              int proTop) {

  int ttl = 0;
  int res = 0;

  Clause learnt;

  if (satis.load()) {
    thnum.fetch_sub(1);
    cond.notify_all();
    return;
  }

  while (!res) {

    if (satis.load()) {
      thnum.fetch_sub(1);
      cond.notify_all();
      return;
    }

    ttl++;

    auto con = prop(litMem, proMem, proTop, varNum);

    if (con != std::nullopt) {

      res = 20;

    } else {

      Clause valMem;

      for (auto &p : *proMem)
        valMem.set(p.lit);

      for (int nex = 1; nex < varNum + 1; nex++)
        if (!valMem.ref[nex]) {

          auto negMem = std::make_shared<ProMem>(*proMem);

          int nexLev = !proMem->size() ? 1 : proMem->back().lev + 1;

          assign(proMem, nex, nexLev, std::nullopt);
          assign(negMem, -nex, nexLev, std::nullopt);

          thnum.fetch_add(1);
          cond.notify_all();
          std::thread negth(karnaugh, varNum, std::ref(litMem), negMem, proTop);

          negth.detach();

          break;
        }
    }
  }

  thnum.fetch_sub(1);
  cond.notify_all();
}

int main(int argc, char **argv) {

  std::cout << "\nc file            " << argv[1] << caRESET "\n";

  LitMem litMem;
  Clause *vals = new Clause();
  vals->rst();

  int varNum;
  int claNum;

  auto beg = Clock::now();

  parse(argv[1], litMem, varNum, claNum);

  // paraRadixSort(litMem, varNum);

  auto mid = Clock::now();
  std::cout << "c elapse::parsing " caBOLD fgBLUE
            << std::chrono::duration_cast<std::chrono::microseconds>(mid - beg)
                   .count()
            << "(us)" caRESET "\n";
  std::cout << "c VARS:           " caBOLD fgGREEN << varNum << caRESET "\n";

  std::shared_ptr<ProMem> proMem = std::make_shared<ProMem>();
  std::thread ini(karnaugh, varNum, std::ref(litMem), proMem, 0);
  ini.detach();

  {
    std::unique_lock<std::mutex> lock(mut);
    cond.wait(lock, [] { return thnum.load() == 0; });
  }

  if (satis) {
    std::cout << caBOLD fgGREEN "s SAT" caRESET << std::endl;
  } else {
    std::cout << caBOLD fgRED "s UNSAT" caRESET << std::endl;
  }

  auto fin = Clock::now();
  std::cout << "c elapse::solving " caBOLD fgBLUE
            << std::chrono::duration_cast<std::chrono::microseconds>(fin - mid)
                   .count()
            << "(us)" caRESET "\n";
  return 0;
}
